package arlab.formulae

/**
 * Created by IntelliJ IDEA.
 * User: Eve
 * Date: 23.02.12
 * Time: 15:54
 * To change this template use File | Settings | File Templates.
 */

// Konjunktion zweier Formeln
case class And(a:Formula, b:Formula) extends Formula {

  override  def toString()={
      "(" + a.toString() + "\u2227" + b.toString() +  ")"
  }
  override def bound()={
    a.bound ++ b.bound
  }
  //Hilfsfunktion für die Bestimmung der freien Variablen
  override def freeHelp(bound:Set[Variable]):Set[Variable]={
    a.freeHelp(bound) ++ b.freeHelp(bound)
  }
  
  //gibt eine Liste zurück die Alle Funktionen mitsammt ihren Stelligkeiten zurückgibt.
  override def functions: Set[(String,Int)] = a.functions ++ b.functions
  
      
  //substituiert alle Variablen aus der uebergebenen map    
  override def subst(sfn: Map[Variable, Term]): Formula =
     And(a.subst(sfn) , b.subst(sfn))
     
     
  override def renameAllVariables(i:Int):Formula = And(a.renameAllVariables(i), b.renameAllVariables(i))
}
